L:Dsys List.
(A,BL.A || B)  {(L)  Dsys & (M:Dsys. (BL. M || B)  M || (L)) & (BL. B  (L))} 

latex

Definitions	P  Q, P  Q, P  Q, x,y. t(x;y), A  B, (x  l), x:A. B(x), A & B, , , Id, (x,yL.P(x;y)), (L), {T}, x. t(x), Prop, l[i], {i..j}, i  j < k, AB, P & Q, A, False, P  Q, A || B, xL. P(x), D1  D2, , MsgA, x:A. B(x), t  T, Dsys
Lemmas	dsys wf, m-sys-compatible wf, int seg wf, l all wf, Id wf, ma-empty wf, m-sys-null-compatible-right, l member wf, m-sys-join wf2, pairwise-cons, pairwise wf, cons member, dsys-compatible-join, d-sub wf, l all cons, dsys-sub-join-left, dsys-sub-join-right, d-sub transitivity